(set-logic QF_BV)
(set-option :model_validate true)
(set-option :model true)
(set-option :unsat_core false)
(set-option :sat.anf true)
(set-option :nlsat.log_lemmas false)
(set-option :sat.local_search false)
(set-option :smt.theory_case_split true)
(set-option :smt.arith.auto_config_simplex false)
(set-option :sat.cut true)
(set-option :smt.arith.random_initial_value false)
;(set-option :sat.unit_walk true)
(set-option :smt.arith.int_eq_branch true)
(set-option :sat.bca false)
(set-option :sat.asymm_branch.all true)
(set-option :nlsat.inline_vars true)
(set-option :nlsat.randomize true)
(set-option :rewriter.blast_eq_value true)
(set-option :sat.branching.anti_exploration true)
(set-option :smt.arith.eager_eq_axioms true)
(set-option :sat.scc false)
(set-option :nlsat.reorder false)
(set-option :smt.arith.greatest_error_pivot false)
(set-option :smt.arith.min false)
(set-option :smt.arith.bprop_on_pivoted_rows false)
(set-option :rewriter.bv_sort_ac false)
(set-option :sat.abce false)
(set-option :sat.acce true)
(set-option :sat.scc.tr true)
(set-option :smt.dack.eq true)
(set-option :sat.bce true)
(set-option :sat.asymm_branch false)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(push 1)
(declare-const v21 Bool)
(push 1)
(pop 1)
(declare-const v22 Bool)
(declare-const bv_24-0 (_ BitVec 24))
(pop 1)
(declare-const bv_14-0 (_ BitVec 14))
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(push 1)
(declare-const v26 Bool)
(declare-const v27 Bool)
(declare-const v28 Bool)
(declare-const bv_16-0 (_ BitVec 16))
(declare-const v29 Bool)
(declare-const v30 Bool)
(declare-const v31 Bool)
(declare-const bv_17-0 (_ BitVec 17))
(declare-const bv_16-2 (_ BitVec 16))
(declare-const v32 Bool)
(pop 1)
(declare-const v33 Bool)
(declare-const v34 Bool)
(declare-const v35 Bool)
(declare-const v36 Bool)
(declare-const v37 Bool)
(push 1)
(declare-const v38 Bool)
(declare-const v39 Bool)
(declare-const v40 Bool)
(declare-const v41 Bool)
(declare-const v42 Bool)
(pop 1)
(declare-const v43 Bool)
(declare-const v44 Bool)
(push 1)
(pop 1)
(declare-const v45 Bool)
(declare-const v46 Bool)
(declare-const v47 Bool)
(declare-const v48 Bool)
(declare-const v49 Bool)
(declare-const v50 Bool)
(push 1)
(declare-const v51 Bool)
(pop 1)
(declare-const v52 Bool)
(declare-const v53 Bool)
(push 1)
(pop 1)
(declare-const v54 Bool)
(declare-const v55 Bool)
(declare-const v56 Bool)
(declare-const v57 Bool)
(declare-const v58 Bool)
(declare-const bv_30-0 (_ BitVec 30))
(declare-const v59 Bool)
(push 1)
(declare-const v60 Bool)
(pop 1)
(declare-const v61 Bool)
(declare-const v62 Bool)
(push 1)
(declare-const v63 Bool)
(declare-const v64 Bool)
(declare-const v65 Bool)
(pop 1)
(declare-const v66 Bool)
(declare-const v67 Bool)
(declare-const v68 Bool)
(declare-const v69 Bool)
(declare-const v70 Bool)
(declare-const v71 Bool)
(declare-const v72 Bool)
(declare-const v73 Bool)
(declare-const v74 Bool)
(declare-const v75 Bool)
(declare-const v76 Bool)
(declare-const v77 Bool)
(declare-const v78 Bool)
(declare-const bv_22-0 (_ BitVec 22))
(declare-const v79 Bool)
(declare-const bv_7-1 (_ BitVec 7))
(declare-const v80 Bool)
(declare-const v81 Bool)
(declare-const bv_8-1 (_ BitVec 8))
(push 1)
(pop 1)
(push 1)
(declare-const v82 Bool)
(declare-const v83 Bool)
(declare-const v84 Bool)
(declare-const v85 Bool)
(declare-const v86 Bool)
(pop 1)
(declare-const v87 Bool)
(declare-const v88 Bool)
(push 1)
(declare-const v89 Bool)
(declare-const v90 Bool)
(pop 1)
(push 1)
(declare-const v91 Bool)
(declare-const v92 Bool)
(declare-const v93 Bool)
(declare-const bv_25-0 (_ BitVec 25))
(pop 1)
(declare-const v94 Bool)
(assert (or v74 v74 v74))
(assert (or v67 v74 v74))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v74 (= (not v18) v58 v10)))
(assert (or v74 (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) v67 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or (= (not v18) v58 v10) v74 v67))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v67 (= (not v18) v58 v10)))
(assert (or v67 (= (not v18) v58 v10) (= (not v18) v58 v10)))
(assert (or v74 v67 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0)))))
(assert (or (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) v67 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v74 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or v74 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) v74))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or v74 (= (not v18) v58 v10) v67))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) v67))
(assert (or v67 (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or v74 (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) v74))
(assert (or (= (not v18) v58 v10) v67 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (= (not v18) v58 v10)))
(assert (or v74 v67 v67))
(assert (or (= (not v18) v58 v10) v74 v74))
(assert (or (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (= (not v18) v58 v10) v67))
(assert (or (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0)))))
(assert (or v74 (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) v67))
(assert (or (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= (not v18) v58 v10) v74))
(assert (or (= (not v18) v58 v10) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0)))))
(assert (or v74 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0)))))
(assert (or v74 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) (= (not v18) v58 v10)))
(assert (or (= (not v18) v58 v10) (= (not v18) v58 v10) v67))
(assert (or v74 v74 (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0)))))
(assert (or (= (not v18) v58 v10) v74 v74))
(assert (or v74 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v74))
(assert (or (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0)))))
(assert (or v74 (= (not v18) v58 v10) v67))
(assert (or (= (not v18) v58 v10) v74 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or (= (not v18) v58 v10) v74 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= (not v18) v58 v10)))
(assert (or (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or v67 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v67 (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or v67 (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0))))
(assert (or v67 v74 (= (not v18) v58 v10)))
(assert (or (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v67 v67))
(assert (or v74 (distinct (bvshl bv_14-0 bv_14-0) (bvadd (bvshl bv_14-0 bv_14-0) (bvshl bv_14-0 bv_14-0))) (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36))))
(assert (or (=> (distinct bv_30-0 bv_30-0 bv_30-0) (= v8 (not v18) v36)) (= ((_ repeat 9) bv_30-0) ((_ repeat 9) bv_30-0)) v74))
(check-sat)
(exit)
